An important design choice : if a function consumes a structure containing mutable borrows for, say, some lifetime 'a, then the backward function returns the whole structure, where only the fields for the mutable borrows have been updated.
For instance, I put this in the tests:

struct MutWrapper2<'a, 'b, T> {
    x: &'a mut T,
    y: &'b mut T,
}

impl<'a, 'b, T> MutWrapper2<'a, 'b, T> {
    fn unwrap(self: Self) -> (&'a mut T, &'b mut T) {
        (self.x, self.y)
    }
}

The generated model is as follows:

structure MutWrapper2 (T : Type) where
  x : T
  y : T

def MutWrapper2.unwrap
  {T : Type} (self : MutWrapper2 T) :
  Result ((T × T) × (T → MutWrapper2 T) × (T → MutWrapper2 T))
  :=
  let back'a := fun ret => { self with x := ret }
  let back'b := fun ret => { self with y := ret }
  Result.ok ((self.x, self.y), back'a, back'b)

This might seem like a strange choice, as we could also generate the following model:

def MutWrapper2.unwrap
  {T : Type} (self : MutWrapper2 T) :
  Result ((T × T) × (T → T) × (T → T))
  :=
  let back'a := fun ret => ret
  let back'b := fun ret => ret
  Result.ok ((self.x, self.y), back'a, back'b)

(i.e., the backward functions give back exactly the tuple of updated fields)

I made this choice because it is not possible to do so for (recursive) enumerations, unless we introduce auxiliary definitions (one auxiliary definition for each lifetime which is used by mutable borrows in the enumeration, to "collect" exactly the values that need to be given back), and doing this would be extremely cumbersome. In prevision of the future support for enumerations with borrows, I decided to make the treatment of ADTs consistent (I do not want to differentiate structures from enumerations at this point). Of course, for structures we could switch between the two treatments through an option (though the presence of such an option would likely make it difficult to handle definitions coming from the standard library).

Also, an important note: the type analysis I do to compute what backward functions consume/produce is unsound if indirections introduced by trait impls are not removed (this PR - this is not a fundamental problem, I just need to put a bit more engineering time into properly handling this), and if there are constraints over associated types (which would be removed by this). For now I generate errors if I detect those, and I added an option to downgrade those errors to warnings, so that the trait.rs test goes through.

Awesome! Does this resolve #75?

Yes it does! I'm marking it as "resolved"